SESAxioms{i:l}
SESAxioms(E; T; pred?; info; when; after)
== (e:E, l:IdLnk.
== (e':E.
== (e'':E.
== (rcv?(e'')  sender(e'') = e  link(e'') = l  e'' = e'  e'' < e' & loc(e') = destination(l))
== & (e, e':E. loc(e) = loc(e')  pred?(e) = pred?(e')  e = e')
== & & SWellFounded(pred!(e;e'))
== & & (e:E. first(e)  loc(pred(e)) = loc(e))
== & & (e:E. rcv?(e)  loc(sender(e)) = source(link(e)))
== & & (e, e':E. rcv?(e)  rcv?(e')  link(e) = link(e')  sender(e) < sender(e')  e < e')
== & & (e:E. first(e)  (x:Id. when(x,e) = after(x,pred(e)))) 

latex

---

clarification:

SESAxioms{i:l}
SESAxioms(E; T; pred?; info; when; after)
== (e:E, l:IdLnk.
== (e':E.
== (e'':E.
== (rcv?(info;e'')
== ( sender(info;e'') = e  E
== ( link(info;e'') = l  IdLnk
== ( e'' = e'  E  cless(E;pred?;info;e'';e') & loc(info;e') = destination(l)  Id)
== & (e:E, e':E. loc(info;e) = loc(info;e')  Id  pred?(e) = pred?(e')  E+Unit  e = e'  E)
== & & strongwellfounded(E; e,e'.pred!(E;pred?;info;e;e'))
== & & (e:E. first(pred?;e)  loc(info;pred(pred?;e)) = loc(info;e)  Id)
== & & (e:E. rcv?(info;e)  loc(info;sender(info;e)) = source(link(info;e))  Id)
== & & (e:E, e':E.
== & & (rcv?(info;e)
== & & ( rcv?(info;e')
== & & ( link(info;e) = link(info;e')  IdLnk
== & & ( cless(E;pred?;info;sender(info;e);sender(info;e'))
== & & ( cless(E;pred?;info;e;e'))
== & & (e:E.
== & & (first(pred?;e)  (x:Id. when(x,e) = after(x,pred(pred?;e))  T(loc(info;e),x))) 

latex

Definitions	x:A. B(x), P  Q, destination(l), A & B, Unit, SWellFounded(R(x;y)), pred!(e;e'), P & Q, source(l), rcv?(e), IdLnk, link(e), sender(e), e < e', P  Q, A, b, first(e), x:A. B(x), Id, loc(e), pred(e)
FDL editor aliases	SESAxioms